
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">

<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<title>Module ErgoSpec.Translation.ErgotoErgoC</title>
<meta name="description" content="Documentation of Coq module ErgoSpec.Translation.ErgotoErgoC" />
<link href="coq2html.css" rel="stylesheet" type="text/css" />
<script type="text/javascript" src="coq2html.js"> </script>
</head>

<body onload="hideAll('proofscript')">
<h1 class="title">Module ErgoSpec.Translation.ErgotoErgoC</h1>
<div class="coq">
<br/>
<div class="doc">Translates contract logic to calculus </div>
<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html">String</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html">List</a></span>.<br/>
<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html">ErgoSpec.Backend.ErgoBackend</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Utils.Misc.html">ErgoSpec.Common.Utils.Misc</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html">ErgoSpec.Common.Utils.Provenance</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html">ErgoSpec.Common.Utils.Names</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html">ErgoSpec.Common.Utils.Result</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html">ErgoSpec.Common.Types.ErgoType</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html">ErgoSpec.Ergo.Lang.Ergo</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html">ErgoSpec.ErgoC.Lang.ErgoC</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCSugar.html">ErgoSpec.ErgoC.Lang.ErgoCSugar</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html">ErgoSpec.Translation.ErgoCompContext</a></span>.<br/>
<br/>
<span class="kwd">Section</span> <span class="id"><a name="ErgotoErgoC">ErgotoErgoC</a></span>.<br/>
&nbsp;&nbsp;<span class="kwd">Context</span> {<span class="id">bm</span>:<span class="id"><a href="https://querycert.github.io/html/Qcert.Common.TypeSystem.TBrandModel.html#brand_model">brand_model</a></span>}.<br/>
<br/>
<div class="doc">Translate Ergo expression to calculus </div>
&nbsp;&nbsp;<span class="kwd">Fixpoint</span> <span class="id"><a name="ergo_expr_to_ergoc_expr">ergo_expr_to_ergoc_expr</a></span> (<span class="id">ctxt</span>:<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span>) (<span class="id">e</span>:<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_expr">laergo_expr</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_expr">ergoc_expr</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#e">e</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EThisContract">EThisContract</a></span> <span class="id">prov</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_current_contract">compilation_context_current_contract</a></span>) <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#use_contract_not_in_contract_error">use_contract_not_in_contract_error</a></span> <span class="id">prov</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">_</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> (<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCSugar.html#thisContract">thisContract</a></span> <span class="id">prov</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EThisClause">EThisClause</a></span> <span class="id">prov</span> =&gt; <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_current_clause">compilation_context_current_clause</a></span>) <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#not_in_clause_error">not_in_clause_error</a></span> <span class="id">prov</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">clause_name</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> (<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCSugar.html#thisClause">thisClause</a></span> <span class="id">prov</span> <span class="id">clause_name</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EThisState">EThisState</a></span> <span class="id">prov</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> (<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCSugar.html#thisState">thisState</a></span> <span class="id">prov</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EVar">EVar</a></span> <span class="id">prov</span> <span class="id">v</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EVar">EVar</a></span> <span class="id">prov</span> <span class="id">v</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EConst">EConst</a></span> <span class="id">prov</span> <span class="id">d</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EConst">EConst</a></span> <span class="id">prov</span> <span class="id">d</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ENone">ENone</a></span> <span class="id">prov</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ENone">ENone</a></span> <span class="id">prov</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ESome">ESome</a></span> <span class="id">prov</span> <span class="id">e</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ESome">ESome</a></span> <span class="id">prov</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_expr_to_ergoc_expr">ergo_expr_to_ergoc_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#e">e</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EArray">EArray</a></span> <span class="id">prov</span> <span class="id">el</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">init_el</span> := <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">proc_one</span> (<span class="id">e</span>:<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_expr">laergo_expr</a></span>) (<span class="id">acc</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_expr">ergoc_expr</a></span>)) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_expr">ergoc_expr</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#cons">cons</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_expr_to_ergoc_expr">ergo_expr_to_ergoc_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#e">e</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#acc">acc</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EArray">EArray</a></span> <span class="id">prov</span>) (<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#fold_right">fold_right</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#proc_one">proc_one</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#init_el">init_el</a></span> <span class="id">el</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EUnaryOp">EUnaryOp</a></span> <span class="id">prov</span> <span class="id">u</span> <span class="id">e</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EUnaryOp">EUnaryOp</a></span> <span class="id">prov</span> <span class="id">u</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_expr_to_ergoc_expr">ergo_expr_to_ergoc_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#e">e</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EBinaryOp">EBinaryOp</a></span> <span class="id">prov</span> <span class="id">b</span> <span class="id">e1</span> <span class="id">e2</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EBinaryOp">EBinaryOp</a></span> <span class="id">prov</span> <span class="id">b</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_expr_to_ergoc_expr">ergo_expr_to_ergoc_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id">e1</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_expr_to_ergoc_expr">ergo_expr_to_ergoc_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id">e2</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EIf">EIf</a></span> <span class="id">prov</span> <span class="id">e1</span> <span class="id">e2</span> <span class="id">e3</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift3">elift3</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EIf">EIf</a></span> <span class="id">prov</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_expr_to_ergoc_expr">ergo_expr_to_ergoc_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id">e1</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_expr_to_ergoc_expr">ergo_expr_to_ergoc_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id">e2</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_expr_to_ergoc_expr">ergo_expr_to_ergoc_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id">e3</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ELet">ELet</a></span> <span class="id">prov</span> <span class="id">v</span> <span class="id">ta</span> <span class="id">e1</span> <span class="id">e2</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ELet">ELet</a></span> <span class="id">prov</span> <span class="id">v</span> <span class="id">ta</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_expr_to_ergoc_expr">ergo_expr_to_ergoc_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id">e1</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_expr_to_ergoc_expr">ergo_expr_to_ergoc_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id">e2</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ENew">ENew</a></span> <span class="id">prov</span> <span class="id">cr</span> <span class="id">el</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">if</span> <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#is_abstract_class">is_abstract_class</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id">cr</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">then</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ECompilationError">ECompilationError</a></span> <span class="id">prov</span> ("<span class="id">Cannot</span> <span class="id">create</span> <span class="id">instance</span> <span class="id">of</span> <span class="id">abstract</span> <span class="id">type</span> `" ++ <span class="id">cr</span> ++ "'"))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">else</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">init_rec</span> := <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">proc_one</span> (<span class="id">att</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_expr">laergo_expr</a></span>) (<span class="id">acc</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_expr">ergoc_expr</a></span>))) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">attname</span> := <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#att">att</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">e</span> := <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_expr_to_ergoc_expr">ergo_expr_to_ergoc_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#snd">snd</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#att">att</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span> (<span class="kwd">fun</span> <span class="id">e</span> =&gt; <span class="kwd">fun</span> <span class="id">acc</span> =&gt; (<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#attname">attname</a></span>,<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#e">e</a></span>)::<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#acc">acc</a></span>) <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#e">e</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#acc">acc</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ENew">ENew</a></span> <span class="id">prov</span> <span class="id">cr</span>) (<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#fold_right">fold_right</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#proc_one">proc_one</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#init_rec">init_rec</a></span> <span class="id">el</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ERecord">ERecord</a></span> <span class="id">prov</span> <span class="id">el</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">init_rec</span> := <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">proc_one</span> (<span class="id">att</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_expr">laergo_expr</a></span>) (<span class="id">acc</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_expr">ergoc_expr</a></span>))) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">attname</span> := <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#att">att</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">e</span> := <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_expr_to_ergoc_expr">ergo_expr_to_ergoc_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#snd">snd</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#att">att</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span> (<span class="kwd">fun</span> <span class="id">e</span> =&gt; <span class="kwd">fun</span> <span class="id">acc</span> =&gt; (<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#attname">attname</a></span>,<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#e">e</a></span>)::<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#acc">acc</a></span>) <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#e">e</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#acc">acc</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ERecord">ERecord</a></span> <span class="id">prov</span>) (<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#fold_right">fold_right</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#proc_one">proc_one</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#init_rec">init_rec</a></span> <span class="id">el</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ECallFun">ECallFun</a></span> <span class="id">prov</span> <span class="id">fname</span> <span class="id">el</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">init_el</span> := <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">proc_one</span> (<span class="id">e</span>:<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_expr">laergo_expr</a></span>) (<span class="id">acc</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_expr">ergoc_expr</a></span>)) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_expr">ergoc_expr</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#cons">cons</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_expr_to_ergoc_expr">ergo_expr_to_ergoc_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#e">e</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#acc">acc</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ECallFun">ECallFun</a></span> <span class="id">prov</span> <span class="id">fname</span>) (<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#fold_right">fold_right</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#proc_one">proc_one</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#init_el">init_el</a></span> <span class="id">el</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ECallFunInGroup">ECallFunInGroup</a></span> <span class="id">prov</span> <span class="id">gname</span> <span class="id">fname</span> <span class="id">el</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">init_el</span> := <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">proc_one</span> (<span class="id">e</span>:<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_expr">laergo_expr</a></span>) (<span class="id">acc</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_expr">ergoc_expr</a></span>)) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_expr">ergoc_expr</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#cons">cons</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_expr_to_ergoc_expr">ergo_expr_to_ergoc_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#e">e</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#acc">acc</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ECallFunInGroup">ECallFunInGroup</a></span> <span class="id">prov</span> <span class="id">gname</span> <span class="id">fname</span>) (<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#fold_right">fold_right</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#proc_one">proc_one</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#init_el">init_el</a></span> <span class="id">el</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EMatch">EMatch</a></span> <span class="id">prov</span> <span class="id">e0</span> <span class="id">ecases</span> <span class="id">edefault</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">ec0</span> := <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_expr_to_ergoc_expr">ergo_expr_to_ergoc_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id">e0</span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">eccases</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">proc_one</span> <span class="id">acc</span> <span class="id">ecase</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eolift">eolift</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">acc</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="kwd">fun</span> <span class="id">x</span> =&gt; (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ecase">ecase</a></span>, <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#x">x</a></span>)::<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#acc">acc</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_expr_to_ergoc_expr">ergo_expr_to_ergoc_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#snd">snd</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ecase">ecase</a></span>))) <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#acc">acc</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#fold_left">fold_left</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#proc_one">proc_one</a></span> <span class="id">ecases</span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">ecdefault</span> := <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_expr_to_ergoc_expr">ergo_expr_to_ergoc_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id">edefault</span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eolift">eolift</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">ec0</span> : <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_expr">ergoc_expr</a></span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eolift">eolift</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">eccases</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">ecdefault</span> : <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_expr">ergoc_expr</a></span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EMatch">EMatch</a></span> <span class="id">prov</span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ec0">ec0</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#eccases">eccases</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ecdefault">ecdefault</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ecdefault">ecdefault</a></span>) <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#eccases">eccases</a></span>) <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ec0">ec0</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EForeach">EForeach</a></span> <span class="id">prov</span> <span class="id">foreachs</span> <span class="id">econd</span> <span class="id">e2</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">init_e2</span> := <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EUnaryOp">EUnaryOp</a></span> <span class="id">prov</span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#OpBag">OpBag</a></span>) (<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_expr_to_ergoc_expr">ergo_expr_to_ergoc_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id">e2</span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">init_e</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id">econd</span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">econd</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">econd</span> <span class="id">e2</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EIf">EIf</a></span> <span class="id">prov</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#econd">econd</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#e2">e2</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EConst">EConst</a></span> <span class="id">prov</span> (<span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#dcoll">dcoll</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>)))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_expr_to_ergoc_expr">ergo_expr_to_ergoc_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id">econd</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#init_e2">init_e2</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt; <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#init_e2">init_e2</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">proc_one</span> (<span class="id">foreach</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_expr">laergo_expr</a></span>) (<span class="id">acc</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_expr">ergoc_expr</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_expr">ergoc_expr</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">v</span> := <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#foreach">foreach</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">e</span> := <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_expr_to_ergoc_expr">ergo_expr_to_ergoc_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#snd">snd</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#foreach">foreach</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EUnaryOp">EUnaryOp</a></span> <span class="id">prov</span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#OpFlatten">OpFlatten</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eolift">eolift</a></span> (<span class="kwd">fun</span> <span class="id">single</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EForeach">EForeach</a></span> <span class="id">prov</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;((<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#v">v</a></span>,<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#single">single</a></span>)::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span>) <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#acc">acc</a></span>) <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#e">e</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#fold_right">fold_right</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#proc_one">proc_one</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#init_e">init_e</a></span> <span class="id">foreachs</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
<div class="doc">Translate an Ergo statement to an Ergo expression </div>
&nbsp;&nbsp;<span class="kwd">Fixpoint</span> <span class="id"><a name="ergo_stmt_to_expr">ergo_stmt_to_expr</a></span> (<span class="id">ctxt</span>:<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span>) (<span class="id">s</span>:<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_stmt">laergo_stmt</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_expr">ergoc_expr</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#s">s</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#SReturn">SReturn</a></span> <span class="id">prov</span> <span class="id">e</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="kwd">fun</span> <span class="id">e</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCSugar.html#ESuccess">ESuccess</a></span> <span class="id">prov</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCSugar.html#mkResult">mkResult</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id">prov</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#e">e</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EVar">EVar</a></span> <span class="id">prov</span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#local_state">local_state</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EVar">EVar</a></span> <span class="id">prov</span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#local_emit">local_emit</a></span>)))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_expr_to_ergoc_expr">ergo_expr_to_ergoc_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id">e</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#SFunReturn">SFunReturn</a></span> <span class="id">prov</span> <span class="id">e</span> =&gt; <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_expr_to_ergoc_expr">ergo_expr_to_ergoc_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id">e</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#SThrow">SThrow</a></span> <span class="id">prov</span> <span class="id">e</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCSugar.html#EError">EError</a></span> <span class="id">prov</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_expr_to_ergoc_expr">ergo_expr_to_ergoc_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id">e</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#SCallClause">SCallClause</a></span> <span class="id">prov</span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EThisContract">EThisContract</a></span> <span class="id">_</span>) <span class="id">clname</span> <span class="id">el</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_current_contract">compilation_context_current_contract</a></span>) <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#call_clause_not_in_contract_error">call_clause_not_in_contract_error</a></span> <span class="id">prov</span> <span class="id">clname</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">coname</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">params</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">if</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string_dec">string_dec</a></span> <span class="id">clname</span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#clause_init_name">clause_init_name</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">then</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;((<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EVar">EVar</a></span> <span class="id">prov</span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#current_time">current_time</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;::(<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCSugar.html#thisContract">thisContract</a></span> <span class="id">prov</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;::(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EConst">EConst</a></span> <span class="id">prov</span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#dunit">dunit</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;::(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EVar">EVar</a></span> <span class="id">prov</span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#local_emit">local_emit</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;::<span class="id">el</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">else</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;((<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EVar">EVar</a></span> <span class="id">prov</span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#current_time">current_time</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;::(<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCSugar.html#thisContract">thisContract</a></span> <span class="id">prov</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;::(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EVar">EVar</a></span> <span class="id">prov</span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#local_state">local_state</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;::(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EVar">EVar</a></span> <span class="id">prov</span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#local_emit">local_emit</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;::<span class="id">el</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">el</span> := <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#emaplift">emaplift</a></span> (<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_expr_to_ergoc_expr">ergo_expr_to_ergoc_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span>) <span class="id">el</span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="kwd">fun</span> <span class="id">el</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ECallFunInGroup">ECallFunInGroup</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id">prov</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id">coname</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id">clname</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#params">params</a></span>) <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#el">el</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#SCallClause">SCallClause</a></span> <span class="id">_</span> <span class="id">e0</span> <span class="id">_</span> <span class="id">_</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#clause_call_not_on_contract_error">clause_call_not_on_contract_error</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#expr_annot">expr_annot</a></span> <span class="id">e0</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#SSetState">SSetState</a></span> <span class="id">prov</span> <span class="id">e1</span> <span class="id">s2</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span> (<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCSugar.html#setState">setState</a></span> <span class="id">prov</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_expr_to_ergoc_expr">ergo_expr_to_ergoc_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id">e1</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_stmt_to_expr">ergo_stmt_to_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id">s2</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#SEmit">SEmit</a></span> <span class="id">prov</span> <span class="id">e1</span> <span class="id">s2</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span> (<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCSugar.html#pushEmit">pushEmit</a></span> <span class="id">prov</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_expr_to_ergoc_expr">ergo_expr_to_ergoc_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id">e1</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_stmt_to_expr">ergo_stmt_to_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id">s2</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#SLet">SLet</a></span> <span class="id">prov</span> <span class="id">vname</span> <span class="id">vtype</span> <span class="id">e1</span> <span class="id">s2</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ELet">ELet</a></span> <span class="id">prov</span> <span class="id">vname</span> <span class="id">vtype</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_expr_to_ergoc_expr">ergo_expr_to_ergoc_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id">e1</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_stmt_to_expr">ergo_stmt_to_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id">s2</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#SIf">SIf</a></span> <span class="id">prov</span> <span class="id">e1</span> <span class="id">s2</span> <span class="id">s3</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift3">elift3</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EIf">EIf</a></span> <span class="id">prov</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_expr_to_ergoc_expr">ergo_expr_to_ergoc_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id">e1</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_stmt_to_expr">ergo_stmt_to_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id">s2</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_stmt_to_expr">ergo_stmt_to_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id">s3</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#SEnforce">SEnforce</a></span> <span class="id">prov</span> <span class="id">e1</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> <span class="id">s3</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift3">elift3</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EIf">EIf</a></span> <span class="id">prov</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EUnaryOp">EUnaryOp</a></span> <span class="id">prov</span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#OpNeg">OpNeg</a></span>) (<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_expr_to_ergoc_expr">ergo_expr_to_ergoc_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id">e1</span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> (<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCSugar.html#EError">EError</a></span> <span class="id">prov</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EConst">EConst</a></span> <span class="id">prov</span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#enforce_error_content">enforce_error_content</a></span> <span class="id">prov</span> ""))))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_stmt_to_expr">ergo_stmt_to_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id">s3</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#SEnforce">SEnforce</a></span> <span class="id">prov</span> <span class="id">e1</span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">s2</span>) <span class="id">s3</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift3">elift3</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EIf">EIf</a></span> <span class="id">prov</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EUnaryOp">EUnaryOp</a></span> <span class="id">prov</span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#OpNeg">OpNeg</a></span>) (<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_expr_to_ergoc_expr">ergo_expr_to_ergoc_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id">e1</span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_stmt_to_expr">ergo_stmt_to_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id">s2</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_stmt_to_expr">ergo_stmt_to_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id">s3</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#SMatch">SMatch</a></span> <span class="id">prov</span> <span class="id">e0</span> <span class="id">scases</span> <span class="id">sdefault</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">ec0</span> := <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_expr_to_ergoc_expr">ergo_expr_to_ergoc_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id">e0</span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">sccases</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">proc_one</span> <span class="id">acc</span> <span class="id">scase</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eolift">eolift</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">acc</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="kwd">fun</span> <span class="id">x</span> =&gt; (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#scase">scase</a></span>, <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#x">x</a></span>)::<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#acc">acc</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_stmt_to_expr">ergo_stmt_to_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#snd">snd</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#scase">scase</a></span>))) <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#acc">acc</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#fold_left">fold_left</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#proc_one">proc_one</a></span> <span class="id">scases</span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">scdefault</span> := <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_stmt_to_expr">ergo_stmt_to_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id">sdefault</span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eolift">eolift</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">ec0</span> : <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_expr">ergoc_expr</a></span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eolift">eolift</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">sccases</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">scdefault</span> : <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_expr">ergoc_expr</a></span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EMatch">EMatch</a></span> <span class="id">prov</span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ec0">ec0</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#sccases">sccases</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#scdefault">scdefault</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#scdefault">scdefault</a></span>) <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#sccases">sccases</a></span>) <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ec0">ec0</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="ergo_stmt_to_expr_top">ergo_stmt_to_expr_top</a></span> (<span class="id">ctxt</span>:<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span>) (<span class="id">prov</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#provenance">provenance</a></span>) (<span class="id">e</span>:<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ergo_stmt">ergo_stmt</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_expr">ergoc_expr</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="kwd">fun</span> <span class="id">e</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ELet">ELet</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#prov">prov</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Names.html#local_state">local_state</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EVar">EVar</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#prov">prov</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#this_state">this_state</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ELet">ELet</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#prov">prov</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#local_emit">local_emit</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EVar">EVar</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#prov">prov</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#this_emit">this_emit</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#e">e</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_stmt_to_expr">ergo_stmt_to_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#e">e</a></span>).<br/>
<br/>
<div class="doc">Translate a clause to clause+calculus </div>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="clause_to_calculus">clause_to_calculus</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ctxt</span>:<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">tem</span>:<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#laergo_type">laergo_type</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">sta</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#option">option</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#laergo_type">laergo_type</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">c</span>:<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_clause">laergo_clause</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Names.html#local_name">local_name</a></span> * <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_function">ergoc_function</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">ctxt</span> : <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span> := <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#set_current_clause">set_current_clause</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#c">c</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#clause_name">clause_name</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">prov</span> := <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#ProvClause">ProvClause</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#loc_of_provenance">loc_of_provenance</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#c">c</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#clause_annot">clause_annot</a></span>)) <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#c">c</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#clause_name">clause_name</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">emit_type</span> := <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#lift_default_emits_type">lift_default_emits_type</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#prov">prov</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#c">c</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#clause_sig">clause_sig</a></span>).(<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#type_signature_emits">type_signature_emits</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">state_type</span> :=  <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#lift_default_state_type">lift_default_state_type</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#prov">prov</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#sta">sta</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">throw_type</span> := <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#default_throws_type">default_throws_type</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#prov">prov</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">output_type</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">response_type</span>' := <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#c">c</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#clause_sig">clause_sig</a></span>).(<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#type_signature_output">type_signature_output</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id">response_type</span>' <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">response_type</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">success_type</span> := <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#mk_success_type">mk_success_type</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#prov">prov</a></span> <span class="id">response_type</span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#state_type">state_type</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#emit_type">emit_type</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">error_type</span> := <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#mk_error_type">mk_error_type</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#prov">prov</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#throw_type">throw_type</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#mk_output_type">mk_output_type</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#prov">prov</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#success_type">success_type</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#error_type">error_type</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">body</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#c">c</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#clause_body">clause_body</a></span>) <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">stmt</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_stmt_to_expr_top">ergo_stmt_to_expr_top</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#prov">prov</a></span> <span class="id">stmt</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">clname</span> := <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#c">c</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#clause_name">clause_name</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">params</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">if</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string_dec">string_dec</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#clname">clname</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#clause_init_name">clause_init_name</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">then</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;((<span class="id"><a href="ErgoSpec.Common.Utils.Names.html#current_time">current_time</a></span>, (<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeDateTime">ErgoTypeDateTime</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#prov">prov</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;::(<span class="id"><a href="ErgoSpec.Common.Utils.Names.html#this_contract">this_contract</a></span>, <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#tem">tem</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;::(<span class="id"><a href="ErgoSpec.Common.Utils.Names.html#this_state">this_state</a></span>, <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeUnit">ErgoTypeUnit</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#prov">prov</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;::(<span class="id"><a href="ErgoSpec.Common.Utils.Names.html#this_emit">this_emit</a></span>, <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeArray">ErgoTypeArray</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#prov">prov</a></span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeNothing">ErgoTypeNothing</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#prov">prov</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;::<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#c">c</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#clause_sig">clause_sig</a></span>).(<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#type_signature_params">type_signature_params</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">else</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;((<span class="id"><a href="ErgoSpec.Common.Utils.Names.html#current_time">current_time</a></span>, (<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeDateTime">ErgoTypeDateTime</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#prov">prov</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;::(<span class="id"><a href="ErgoSpec.Common.Utils.Names.html#this_contract">this_contract</a></span>, <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#tem">tem</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;::(<span class="id"><a href="ErgoSpec.Common.Utils.Names.html#this_state">this_state</a></span>, <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#state_type">state_type</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;::(<span class="id"><a href="ErgoSpec.Common.Utils.Names.html#this_emit">this_emit</a></span>, <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeArray">ErgoTypeArray</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#prov">prov</a></span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeNothing">ErgoTypeNothing</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#prov">prov</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;::<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#c">c</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#clause_sig">clause_sig</a></span>).(<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#type_signature_params">type_signature_params</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">body</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#clname">clname</a></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#mkFuncC">mkFuncC</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#prov">prov</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#mkSigC">mkSigC</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#params">params</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#output_type">output_type</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#body">body</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#body">body</a></span>.<br/>
<br/>
<div class="doc">Translate a function to function+calculus </div>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="function_to_calculus">function_to_calculus</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ctxt</span>:<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">f</span>:<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_function">laergo_function</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_function">ergoc_function</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">prov</span> := <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#f">f</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#function_annot">function_annot</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">body</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#f">f</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#function_body">function_body</a></span>) <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">e</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_expr_to_ergoc_expr">ergo_expr_to_ergoc_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id">e</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#mkFuncC">mkFuncC</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#f">f</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#function_annot">function_annot</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#mkSigC">mkSigC</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#f">f</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#function_sig">function_sig</a></span>).(<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#type_signature_params">type_signature_params</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#f">f</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#function_sig">function_sig</a></span>).(<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#type_signature_output">type_signature_output</a></span>)))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#body">body</a></span>.<br/>
<br/>
<div class="doc">Translate a contract to a contract+calculus </div>
<div class="doc">For a contract, add 'contract' and 'now' to the comp_context </div>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="contract_to_calculus">contract_to_calculus</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ctxt</span>:<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">c</span>:<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_contract">laergo_contract</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_contract">ergoc_contract</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">clauses</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#emaplift">emaplift</a></span> (<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#clause_to_calculus">clause_to_calculus</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#c">c</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#contract_template">contract_template</a></span>) <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#c">c</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#contract_state">contract_state</a></span>)) <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#c">c</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#contract_clauses">contract_clauses</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#mkContractC">mkContractC</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#c">c</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#contract_annot">contract_annot</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#clauses">clauses</a></span>.<br/>
<br/>
<div class="doc">Translate a statement to a statement+calculus </div>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="declaration_to_calculus">declaration_to_calculus</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ctxt</span>:<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">d</span>:<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_declaration">laergo_declaration</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_declaration">ergoc_declaration</a></span> * <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#d">d</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DNamespace">DNamespace</a></span> <span class="id">prov</span> <span class="id">ns</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>, <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DImport">DImport</a></span> <span class="id">prov</span> <span class="id">import</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>, <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DType">DType</a></span> <span class="id">prov</span> <span class="id">ergo_type</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">name</span> := <span class="id">ergo_type</span>.(<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#type_declaration_name">type_declaration_name</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">if</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#in_dec">in_dec</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string_dec">string_dec</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#name">name</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#map">map</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#type_declaration_name">type_declaration_name</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_new_type_decls">compilation_context_new_type_decls</a></span>) ++<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_type_decls">compilation_context_type_decls</a></span>))) <span class="kwd">then</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ECompilationError">ECompilationError</a></span> <span class="id">prov</span> ("<span class="id">Cannot</span> <span class="id">redefine</span> <span class="id">type</span> `" ++ <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#name">name</a></span> ++ "'"))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">else</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>, <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_add_new_type_declaration">compilation_context_add_new_type_declaration</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id">ergo_type</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DStmt">DStmt</a></span> <span class="id">prov</span> <span class="id">s</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">x</span> =&gt; (<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#x">x</a></span>::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>, <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#DCExpr">DCExpr</a></span> <span class="id">prov</span>) (<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_stmt_to_expr_top">ergo_stmt_to_expr_top</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id">prov</span> <span class="id">s</span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DConstant">DConstant</a></span> <span class="id">prov</span> <span class="id">v</span> <span class="id">ta</span> <span class="id">e</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">x</span> =&gt; (<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#x">x</a></span>::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>, <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#DCConstant">DCConstant</a></span> <span class="id">prov</span> <span class="id">v</span> <span class="id">ta</span>) (<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_expr_to_ergoc_expr">ergo_expr_to_ergoc_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id">e</span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DFunc">DFunc</a></span> <span class="id">prov</span> <span class="id">fn</span> <span class="id">f</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">x</span> =&gt; (<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#x">x</a></span>::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>, <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#DCFunc">DCFunc</a></span> <span class="id">prov</span> <span class="id">fn</span>) (<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#function_to_calculus">function_to_calculus</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id">f</span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DContract">DContract</a></span> <span class="id">prov</span> <span class="id">cn</span> <span class="id">c</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">x</span> =&gt; (<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#x">x</a></span>::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>, <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#DCContract">DCContract</a></span> <span class="id">prov</span> <span class="id">cn</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">let</span> <span class="id">ctxt</span> := <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#set_current_contract">set_current_contract</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id">cn</span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#contract_to_calculus">contract_to_calculus</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id">c</span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DSetContract">DSetContract</a></span> <span class="id">prov</span> <span class="id">cn</span> <span class="id">e1</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">ctxt</span> := <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#set_current_contract">set_current_contract</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id">cn</span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">x</span> =&gt; (<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#x">x</a></span> :: (<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#DCConstant">DCConstant</a></span> <span class="id">prov</span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#this_state">this_state</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EConst">EConst</a></span> <span class="id">prov</span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#dunit">dunit</a></span>)) :: <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>,<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#DCConstant">DCConstant</a></span> <span class="id">prov</span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#this_contract">this_contract</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_expr_to_ergoc_expr">ergo_expr_to_ergoc_expr</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id">e1</span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
<div class="doc">Translate a module to a module+calculus </div>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="declarations_calculus">declarations_calculus</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ctxt</span>:<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">dl</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ergo_declaration">ergo_declaration</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_declaration">ergoc_declaration</a></span> * <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">proc_one</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">acc</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_declaration">ergoc_declaration</a></span> * <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">d</span>:<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ergo_declaration">ergo_declaration</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_declaration">ergoc_declaration</a></span> * <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eolift">eolift</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">acc</span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_declaration">ergoc_declaration</a></span> * <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> (<span class="id">acc</span>, <span class="id">ctxt</span>) := <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#acc">acc</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="kwd">fun</span> <span class="id">decls</span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_declaration">ergoc_declaration</a></span> * <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> (<span class="id">decls</span>, <span class="id">ctxt</span>) := <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#decls">decls</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#acc">acc</a></span> ++ <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#decls">decls</a></span>, <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#declaration_to_calculus">declaration_to_calculus</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#d">d</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#acc">acc</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#fold_left">fold_left</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#proc_one">proc_one</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#dl">dl</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>, <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span>)).<br/>
<br/>
<div class="doc">Translate a module to a module+calculus </div>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="ergo_module_to_calculus">ergo_module_to_calculus</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ctxt</span>:<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">p</span>:<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_module">laergo_module</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_module">ergoc_module</a></span> * <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">res</span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_declaration">ergoc_declaration</a></span> * <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> (<span class="id">decls</span>, <span class="id">ctxt</span>) := <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#res">res</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#mkModuleC">mkModuleC</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#p">p</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#module_annot">module_annot</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#p">p</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#module_namespace">module_namespace</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#decls">decls</a></span>, <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#declarations_calculus">declarations_calculus</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#p">p</a></span>.(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#module_declarations">module_declarations</a></span>)).<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="ergo_modules_to_calculus">ergo_modules_to_calculus</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ctxt</span>:<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">pl</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_module">laergo_module</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_module">ergoc_module</a></span> * <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift_context_fold_left">elift_context_fold_left</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ergo_module_to_calculus">ergo_module_to_calculus</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#pl">pl</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ctxt">ctxt</a></span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Section</span> <span class="id"><a name="ErgotoErgoC.Examples">Examples</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="f1">f1</a></span> : <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_function">laergo_function</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#mkFunc">mkFunc</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#mkErgoTypeSignature">mkErgoTypeSignature</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(("<span class="id">rate</span>"%<span class="id">string</span>, <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeDouble">ErgoTypeDouble</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span>)::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeAny">ErgoTypeAny</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EConst">EConst</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> (<span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#dfloat">dfloat</a></span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Float.html#float_one">float_one</a></span>))).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="f2">f2</a></span> : <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_function">laergo_function</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#mkFunc">mkFunc</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#mkErgoTypeSignature">mkErgoTypeSignature</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(("<span class="id">rate</span>"%<span class="id">string</span>, <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeDouble">ErgoTypeDouble</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span>)::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeAny">ErgoTypeAny</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EThisContract">EThisContract</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span>)).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="cl1">cl1</a></span> : <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_clause">laergo_clause</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#mkClause">mkClause</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"<span class="id">volumediscount</span>"%<span class="id">string</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#mkErgoTypeSignature">mkErgoTypeSignature</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(("<span class="id">request</span>"%<span class="id">string</span>, <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeClassRef">ErgoTypeClassRef</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#default_request_absolute_name">default_request_absolute_name</a></span>)::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeAny">ErgoTypeAny</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#SReturn">SReturn</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ECallFun">ECallFun</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> "<span class="id">addFee</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EConst">EConst</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> (<span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#dfloat">dfloat</a></span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Float.html#float_zero">float_zero</a></span>)::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>)))).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="cl2">cl2</a></span> : <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_clause">laergo_clause</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#mkClause">mkClause</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"<span class="id">volumediscount</span>"%<span class="id">string</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#mkErgoTypeSignature">mkErgoTypeSignature</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(("<span class="id">request</span>"%<span class="id">string</span>, <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeClassRef">ErgoTypeClassRef</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#default_request_absolute_name">default_request_absolute_name</a></span>)::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeAny">ErgoTypeAny</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#SReturn">SReturn</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ECallFun">ECallFun</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> "<span class="id">addFee</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EThisContract">EThisContract</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span>::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>)))).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="co1">co1</a></span> : <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_contract">laergo_contract</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#mkContract">mkContract</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeClassRef">ErgoTypeClassRef</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> "<span class="id">TemplateModel</span>"%<span class="id">string</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#cl1">cl1</a></span>::<span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#cl2">cl2</a></span>::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>).<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="dl1">dl1</a></span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_declaration">laergo_declaration</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DFunc">DFunc</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> "<span class="id">addFee</span>"%<span class="id">string</span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#f1">f1</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:: (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DContract">DContract</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> "<span class="id">VolumeDiscount</span>"%<span class="id">string</span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#co1">co1</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:: <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="dl2">dl2</a></span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#laergo_declaration">laergo_declaration</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DFunc">DFunc</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> "<span class="id">addFee</span>"%<span class="id">string</span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#f1">f1</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:: (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DFunc">DFunc</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> "<span class="id">addFee2</span>"%<span class="id">string</span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#f2">f2</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:: (<span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#DContract">DContract</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> "<span class="id">VolumeDiscount</span>"%<span class="id">string</span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#co1">co1</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:: <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ErgotoErgoC.Examples">Examples</a></span>.<br/>
<br/>
<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Translation.ErgotoErgoC.html#ErgotoErgoC">ErgotoErgoC</a></span>.<br/>
<br/>

</div>
<div class="footer"><hr/>Generated by <a href="https://github.com/xavierleroy/coq2html/">coq2html</div>
</body>
</html>
